r:Rng, i, j:.
(i < j)
 (E:({i..j}|r|).
 ((r) i  k < j. E(k)) = (((r) i  k < j - 1. E(k)) +r E(j - 1))  |r|) 

latex

Definitions	t  T, IMonoid, x:A. B(x), t.2, t.1, , P & Q, Mon, Group{i}, AbGrp, r+gp, *, |g|, (r) i  k < j. E(k)
Lemmas	rng wf, abgrp wf, grp id wf, grp op wf, grp car wf, monoid p wf, add grp of rng wf b, mon itop unroll hi